/**
 * Software Analysis and Verification 
 * @project: Verify Pattern Matching with Guards in Scala
 * @authors: Mirco Dotta and Philippe Suter
 */



package ch.epfl.lara.patterns.utils;

import ch.epfl.lara.patterns.ast._

object FormulaSimplifier {
  
  def apply(form: Formula) : Formula = {
    def takeAStep(f: Formula) : Formula = f match {
      case And(True, f) => f
      case And(f, True) => f
      case And(False, f) => False
      case And(f, False) => False
      
      case Or(True, f) => True
      case Or(f, True) => True
      case Or(False, f) => f
      case Or(f, False) => f
      
      case Not(True) => False
      case Not(False) => True
      case Not(Not(f)) => f
      
      case Imply(True, f) => f
      case Imply(f, False) => Not(f)
       
      case And(f1, f2) => And(this(f1), this(f2))
      case Or(f1, f2) => Or(this(f1), this(f2))
      case Not(f) => Not(this(f))
      case Exists(v, f) => Exists(v, this(f))
      case Forall(v, f) => Forall(v, this(f))
      case Imply(f1, f2) => Imply(this(f1),this(f2))
      case True => True
      case False => False
      case _ => f
    }
      
    def maxSteps(f1: Formula) : Formula = {
      val f2 = takeAStep(f1)
      if(f2 equals f1) {
        f1
      } else {
        maxSteps(f2)
      }
    }
    
    maxSteps(form)
  }
  
  
  def isTautology(f: Formula) : Boolean = f match {
    case Equal(t1, t2) if(t1 equals t2) => true
    case _ => false
  }
  
  def isContradiction(f: Formula) : Boolean = f match {
    // to be "improved"
    case _ => false
  }
}
